/-
Copyright (c) 2024 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
module

public import Mathlib.NumberTheory.Real.Irrational
public import Mathlib.Topology.Instances.AddCircle.Defs
public import Mathlib.Topology.Algebra.Order.Archimedean

/-!
# Irrational rotation is minimal

In this file we prove that the multiples of an irrational element of an `AddCircle` are dense.
Moreover, an additive subgroup of the circle is dense
iff it is not generated by a single element of finite additive order.
-/

@[expose] public section

open Set Filter
open scoped Pointwise Topology

/-- The additive subgroup of real numbers generated by `a` and `b` is dense
iff `a / b` is an irrational number.

Here we rely on the fact that `a / 0 = 0` in Mathlib,
so we don't need to add `b ≠ 0` as an assumption. -/
theorem dense_addSubgroupClosure_pair_iff {a b : ℝ} :
    Dense (AddSubgroup.closure {a, b} : Set ℝ) ↔ Irrational (a / b) := by
  rcases eq_or_ne b 0 with rfl | hb
  · rw [pair_comm]
    simpa [← AddSubgroup.zmultiples_eq_closure] using not_denseRange_zsmul
  constructor
  · rintro hd ⟨r, hr⟩
    refine not_denseRange_zsmul (a := b / r.den) <| hd.mono ?_
    rw [← AddSubgroup.coe_zmultiples, SetLike.coe_subset_coe, AddSubgroup.closure_le,
      AddSubgroup.coe_zmultiples, pair_subset_iff]
    refine ⟨⟨r.num, ?_⟩, r.den, ?_⟩
    · simp [field, mul_div_left_comm _ b, ← Rat.cast_def, hr]
    · simp [field]
  · intro h
    contrapose! h
    rcases (AddSubgroup.dense_or_cyclic _).resolve_left h with ⟨c, hc⟩
    have : {a, b} ⊆ range (· • c : ℤ → ℝ) := by
      rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc]
      apply AddSubgroup.subset_closure
    rcases pair_subset_iff.1 this with ⟨⟨m, rfl⟩, n, rfl⟩
    simp_all [mul_div_mul_right]

namespace AddCircle

/-- The multiples of a number `a` are dense on a circle of length `p` iff `a / p` is irrational. -/
theorem denseRange_zsmul_coe_iff {a p : ℝ} :
    DenseRange (· • a : ℤ → AddCircle p) ↔ Irrational (a / p) := by
  rw [← dense_addSubgroupClosure_pair_iff, DenseRange,
    ← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
    ← AddSubgroup.coe_zmultiples, ← AddSubgroup.coe_comap, ← AddMonoidHom.map_zmultiples,
    AddSubgroup.comap_map_eq, QuotientAddGroup.ker_mk', AddSubgroup.zmultiples_eq_closure,
    AddSubgroup.zmultiples_eq_closure, ← AddSubgroup.closure_union, insert_eq]

/-- The multiples of a number `a` are dense on a circle of length `p > 0`
iff `a` has infinite additive order. -/
theorem denseRange_zsmul_iff {p : ℝ} [Fact (0 < p)] {a : AddCircle p} :
    DenseRange (· • a : ℤ → AddCircle p) ↔ addOrderOf a = 0 := by
  rcases QuotientAddGroup.mk_surjective a with ⟨a, rfl⟩
  simp [denseRange_zsmul_coe_iff, isOfFinAddOrder_iff_exists_rat_eq_div, Irrational]

/-- A subgroup of the circle `ℝ⧸pℤ`, `p > 0`, is dense
iff it is not generated by a single element of finite additive order. -/
theorem dense_addSubgroup_iff_ne_zmultiples {p : ℝ} [Fact (0 < p)] {s : AddSubgroup (AddCircle p)} :
    Dense (s : Set (AddCircle p)) ↔ ∀ a, addOrderOf a ≠ 0 → s ≠ .zmultiples a := by
  constructor
  · rintro hd a ha rfl
    rw [AddSubgroup.coe_zmultiples, ← DenseRange, denseRange_zsmul_iff] at hd
    exact ha hd
  · intro h
    contrapose! h
    obtain ⟨a, rfl⟩ : ∃ a, s = .zmultiples a := by
      rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
        ← AddSubgroup.coe_comap, xor_iff_not_iff'.1 (AddSubgroup.dense_xor'_cyclic _)] at h
      rcases h with ⟨a, ha⟩
      use a
      rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha,
        AddSubgroup.map_comap_eq_self_of_surjective]
      exact Quot.mk_surjective
    exact ⟨a, denseRange_zsmul_iff.not.mp h, rfl⟩

end AddCircle
